Nuprl Lemma : fpf-sub-val2 11,40

AA':Type.
strong-subtype(A;A')
 (B:(AType), eq:EqDecider(A'), fg:a:A fp B(a), x:A'PQ:(a:AB(a)).
 (x:Az:B(x). P(x,z Q(x,z))
  g  f
  (z != f(x P(x,z))
  (z != g(x Q(x,z))) 
latex


Definitions(x  l), deq-member(eq;x;L), f(x), P  Q, P & Q, S  T, A c B, b, t  T, EqDecider(T), strong-subtype(A;B), , x(s1,s2), xt(x), z != f(x P(a;z), a:A fp B(a), x  dom(f), x:AB(x), P  Q, f  g, x(s)
Lemmasstrong-subtype-deq-subtype, fpf-sub wf, fpf wf, deq wf, strong-subtype wf, strong-subtype-l member-type, assert-deq-member, deq-member wf, assert wf, l member wf

origin